0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CpxRNTS
↳13 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CpxRNTS
↳15 IntTrsBoundProof (UPPER BOUND(ID), 148 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 50 ms)
↳18 CpxRNTS
↳19 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 842 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 417 ms)
↳24 CpxRNTS
↳25 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 775 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 366 ms)
↳30 CpxRNTS
↳31 FinalProof (⇔, 0 ms)
↳32 BOUNDS(1, n^2)
U11(tt, M, N) → U12(tt, activate(M), activate(N))
U12(tt, M, N) → s(plus(activate(N), activate(M)))
U21(tt, M, N) → U22(tt, activate(M), activate(N))
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
x(N, 0) → 0
x(N, s(M)) → U21(tt, M, N)
activate(X) → X
U11(tt, M, N) → U12(tt, activate(M), activate(N)) [1]
U12(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U21(tt, M, N) → U22(tt, activate(M), activate(N)) [1]
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
plus(N, 0) → N [1]
plus(N, s(M)) → U11(tt, M, N) [1]
x(N, 0) → 0 [1]
x(N, s(M)) → U21(tt, M, N) [1]
activate(X) → X [1]
U11(tt, M, N) → U12(tt, activate(M), activate(N)) [1]
U12(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U21(tt, M, N) → U22(tt, activate(M), activate(N)) [1]
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
plus(N, 0) → N [1]
plus(N, s(M)) → U11(tt, M, N) [1]
x(N, 0) → 0 [1]
x(N, s(M)) → U21(tt, M, N) [1]
activate(X) → X [1]
U11 :: tt → s:0 → s:0 → s:0 tt :: tt U12 :: tt → s:0 → s:0 → s:0 activate :: s:0 → s:0 s :: s:0 → s:0 plus :: s:0 → s:0 → s:0 U21 :: tt → s:0 → s:0 → s:0 U22 :: tt → s:0 → s:0 → s:0 x :: s:0 → s:0 → s:0 0 :: s:0 |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none
(c) The following functions are completely defined:
activate
x
U21
U22
plus
U11
U12
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
0 => 0
U11(z, z', z'') -{ 3 }→ U12(0, M, N) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(N, M) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U21(z, z', z'') -{ 3 }→ U22(0, M, N) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U22(z, z', z'') -{ 4 }→ plus(x(N, M), N) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
plus(z, z') -{ 1 }→ N :|: z = N, z' = 0, N >= 0
plus(z, z') -{ 1 }→ U11(0, M, N) :|: z' = 1 + M, z = N, M >= 0, N >= 0
x(z, z') -{ 1 }→ U21(0, M, N) :|: z' = 1 + M, z = N, M >= 0, N >= 0
x(z, z') -{ 1 }→ 0 :|: z = N, z' = 0, N >= 0
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
{ activate } { plus, U12, U11 } { U22, x, U21 } |
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: ?, size: O(n1) [z] |
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] |
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] |
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] plus: runtime: ?, size: O(n1) [z + z'] U12: runtime: ?, size: O(n1) [1 + z' + z''] U11: runtime: ?, size: O(n1) [1 + z' + z''] |
U11(z, z', z'') -{ 3 }→ U12(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 3 }→ 1 + plus(z'', z') :|: z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
plus(z, z') -{ 1 }→ U11(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] plus: runtime: O(n1) [1 + 7·z'], size: O(n1) [z + z'] U12: runtime: O(n1) [4 + 7·z'], size: O(n1) [1 + z' + z''] U11: runtime: O(n1) [7 + 7·z'], size: O(n1) [1 + z' + z''] |
U11(z, z', z'') -{ 7 + 7·z' }→ s :|: s >= 0, s <= 1 * z' + 1 * z'' + 1, z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 4 + 7·z' }→ 1 + s' :|: s' >= 0, s' <= 1 * z'' + 1 * z', z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 + 7·z' }→ s'' :|: s'' >= 0, s'' <= 1 * (z' - 1) + 1 * z + 1, z' - 1 >= 0, z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] plus: runtime: O(n1) [1 + 7·z'], size: O(n1) [z + z'] U12: runtime: O(n1) [4 + 7·z'], size: O(n1) [1 + z' + z''] U11: runtime: O(n1) [7 + 7·z'], size: O(n1) [1 + z' + z''] |
U11(z, z', z'') -{ 7 + 7·z' }→ s :|: s >= 0, s <= 1 * z' + 1 * z'' + 1, z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 4 + 7·z' }→ 1 + s' :|: s' >= 0, s' <= 1 * z'' + 1 * z', z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 + 7·z' }→ s'' :|: s'' >= 0, s'' <= 1 * (z' - 1) + 1 * z + 1, z' - 1 >= 0, z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] plus: runtime: O(n1) [1 + 7·z'], size: O(n1) [z + z'] U12: runtime: O(n1) [4 + 7·z'], size: O(n1) [1 + z' + z''] U11: runtime: O(n1) [7 + 7·z'], size: O(n1) [1 + z' + z''] U22: runtime: ?, size: O(n2) [z'·z'' + z''] x: runtime: ?, size: O(n2) [z + z·z'] U21: runtime: ?, size: O(n2) [z'·z'' + z''] |
U11(z, z', z'') -{ 7 + 7·z' }→ s :|: s >= 0, s <= 1 * z' + 1 * z'' + 1, z = 0, z' >= 0, z'' >= 0
U12(z, z', z'') -{ 4 + 7·z' }→ 1 + s' :|: s' >= 0, s' <= 1 * z'' + 1 * z', z = 0, z' >= 0, z'' >= 0
U21(z, z', z'') -{ 3 }→ U22(0, z', z'') :|: z = 0, z' >= 0, z'' >= 0
U22(z, z', z'') -{ 4 }→ plus(x(z'', z'), z'') :|: z = 0, z' >= 0, z'' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
plus(z, z') -{ 1 + 7·z' }→ s'' :|: s'' >= 0, s'' <= 1 * (z' - 1) + 1 * z + 1, z' - 1 >= 0, z >= 0
plus(z, z') -{ 1 }→ z :|: z' = 0, z >= 0
x(z, z') -{ 1 }→ U21(0, z' - 1, z) :|: z' - 1 >= 0, z >= 0
x(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0
activate: runtime: O(1) [1], size: O(n1) [z] plus: runtime: O(n1) [1 + 7·z'], size: O(n1) [z + z'] U12: runtime: O(n1) [4 + 7·z'], size: O(n1) [1 + z' + z''] U11: runtime: O(n1) [7 + 7·z'], size: O(n1) [1 + z' + z''] U22: runtime: O(n2) [6 + 9·z' + 7·z'·z'' + 7·z''], size: O(n2) [z'·z'' + z''] x: runtime: O(n2) [11 + 7·z + 7·z·z' + 9·z'], size: O(n2) [z + z·z'] U21: runtime: O(n2) [9 + 9·z' + 7·z'·z'' + 7·z''], size: O(n2) [z'·z'' + z''] |